$\forall$$A$:Type, $P$:($A$$\rightarrow$Prop). strong{-}subtype(\{$x$:$A$$\mid$ $P$($x$) \};$A$)